The Letter and the Court

The letter and the court #

In the age of sail, the difference between a privateer and a pirate was a piece of paper. A letter of marque was a formal commission from a sovereign authorizing a private vessel to attack and capture enemy ships. The letter specified which enemy nation, which waters, and for how long. Without it, the same acts constituted piracy, punishable by hanging. But the letter alone was not sufficient. Privateers brought captured prizes before an admiralty prize court, which evaluated the capture against the letter’s terms: the ship’s papers, its cargo manifest, its port of registry. The court did not ask the privateer what they intended. It evaluated structured evidence against formal rules. When privateers exceeded their letters or false flags confused them, the court caught it. The evaluation was deterministic and independent of the privateer’s judgment.

AI agents carry credentials that say who they are. No credential says what they should be allowed to do right now, for this specific task. The industry is issuing letters without building courts.

The modern deputy #

In 1977, Norm Hardy discovered the structural version of this problem at Tymshare, a commercial timesharing environment. The company’s Fortran compiler needed write access to a system directory to collect language statistics. A user discovered they could specify the system billing file as a debug output target. The compiler wrote there, destroying the billing data. The compiler’s permissions were determined by who it was, not what it was asked to do. Hardy named this the confused deputy and argued that capabilities, tokens that bind authority to specific operations, were the only structural fix. The paper sat in the ACM archives for decades. The agentic web is rediscovering it at scale.

The pattern is active in production. In March 2026, a Meta AI agent exposed sensitive data to unauthorized employees for two hours, passing every identity check the entire time. Nothing in the identity stack distinguished the rogue request from a legitimate one. In September 2025, Salesforce AgentForce’s ForcedLeak vulnerability (CVSS 9.4) let attackers exfiltrate CRM data through an agent using permissions it legitimately held, through an expired domain purchased for five dollars. Both agents did exactly what they were authorized to do. Neither did what any human intended.

I contributed to this pattern myself. In Weighting the Switch, I described scoping my agent’s directory access after granting it blanket write permissions. The fix worked for the blast radius problem. It did not work for the authority problem. Within the permitted directories, the agent could read credential files, modify configuration, and execute scripts. I had scoped where the agent could operate but not what it could do there. The permissions were bound to the agent’s identity, not to the task it was performing. A letter of marque that said “you may operate in the Caribbean” without specifying which ships to target.

In Stamps Without Passports, I identified the gap: IETF working groups are standardizing authentication through drafts like WIMSE and AIMS. Authorization is not. No standard constrains what an agent can do right now, for this specific task, given the current context. This post fills the gap.

Capabilities, not permissions #

In January 2026, Semgrep published “Security Like It’s 1977,” arguing that capability-based security, proposed alongside Hardy’s confused deputy paper, is the structural answer for the agentic web. The argument is precise. Access control lists check who you are, not what you are doing. As Semgrep’s Kurt Boberg put it, “an application you run can do anything you can do.” An agent that inherits your OAuth token inherits your full authority. Mark Miller and Dean Tribble coined the term ambient authority to describe this: permissions determined by identity rather than intent.

A capability is a single unforgeable token that both designates a resource and authorizes a specific operation on it. You cannot name something you cannot touch. Three properties matter for agents. Capabilities are unforgeable: the agent cannot create capabilities it was not given. They are attenuable: when delegating to a sub-agent, the delegator can only pass narrower capabilities, never broader ones. And they are revocable: the issuer can invalidate the capability at any time, without coordinating with the holder.

The Cloud Security Alliance reports that 97% of non-human identities in enterprise environments carry excessive privileges. Each delegation hop in a multi-agent chain compounds the risk. Capabilities invert the default. Instead of granting broad access and hoping the agent stays within bounds, you grant narrow access and the agent cannot exceed it regardless of what the model decides.

The policy that proves itself #

Cedar is an open-source authorization policy language designed for this problem. Policies evaluate structured requests against formal logic. The model never sees the policy. The model cannot influence it. As I argued in The Linguistic Von Neumann Bottleneck, the policy gateway evaluates the request against deterministic rules. It denies the request regardless of what the model, or the injection, decided. But deterministic evaluation raises a harder question: how do you know the policy engine itself is correct?

Cedar answers this with formal verification. The Cedar team built an executable formal model of the language in the Lean theorem prover and proved correctness properties, including authorization soundness and validator type safety, mathematically. This is not testing. Testing proves the presence of correct behavior for specific inputs. Formal verification proves the absence of incorrect behavior for all possible inputs. The distinction matters. An attacker who bypasses a tested system found an input no one checked. An attacker who bypasses a formally verified system found a flaw in mathematics.

The most consequential proven property is that forbids always override permits. If any forbid policy in your policy set is satisfied by a request, the authorization decision is deny, regardless of how many permit policies are also satisfied. The Lean proof:

theorem forbid_trumps_permit
  (request : Request) (entities : Entities) (policies : Policies) :
  (IsExplicitlyForbidden request entities policies) →
  (isAuthorized request entities policies).decision = .deny
:= by
  intro h
  unfold isAuthorized
  rw [explicitly_forbidden_iff_satisfying_forbid] at h
  simp [h]

The theorem states: for any request, any set of entities, and any collection of policies, if a forbid policy is satisfied, the result is deny. The proof is four lines of tactics. It covers every possible input. No test suite, however large, offers this guarantee. The Cedar team maintains 1,673 lines of Lean model alongside 5,714 lines of proofs and 24,915 lines of Rust production code. The validator soundness proof alone, which guarantees that accepted policies cannot produce type errors during evaluation, required 4,686 lines and eighteen person-days to develop. Millions of randomly generated test cases run nightly to confirm the Rust production code matches the Lean model.

This is the authorization equivalent of the NX bit. In The Linguistic Von Neumann Bottleneck, I argued that the NX bit does not make buffer overflows unlikely. It makes them impossible by enforcing a hardware invariant: memory is writable or executable, never both. Cedar’s formal verification does not make policy violations unlikely. It makes them impossible for the properties that are proven. The forbid-trumps-permit invariant holds for every request the engine will ever evaluate, not because someone tested it, but because someone proved it.

This guarantee is possible because Cedar is deliberately not Turing-complete. The halting problem tells us that no algorithm can determine whether an arbitrary program will terminate. A Turing-complete policy language like Rego inherits this limitation: you cannot prove, in general, that a Rego policy set will always produce a decision. You can test it extensively. You cannot prove it universally. Cedar’s language is decidable. Every evaluation terminates. Every policy set produces a decision. The formal proofs exist because the language is restricted. If Cedar were more expressive, the proofs would be impossible.

Cedar also evaluates 42 to 60 times faster than Open Policy Agent (OPA) Rego, sub-millisecond even across hundreds of policies. The cost of deterministic, formally verified authorization is not latency.

Delegation as data #

Phil Windley’s series on Cedar and OpenClaw demonstrated that developers can model delegation as data and enforce it through a stable policy set. This post extends that pattern with the risk tier framework from Weighting the Switch and the scope attenuation requirements from Stamps Without Passports.

Consider a three-hop delegation chain. A user delegates to a customer-support agent, which delegates to an order-processor agent. Each hop must narrow scope. The RFC 8693 delegation token that reaches the order-processor carries the full chain in its act claims:

{
  "aud": "https://api.inventory.example.com",
  "iss": "https://as.example.com",
  "exp": 1711540200,
  "nbf": 1711539300,
  "sub": "jchen@example.com",
  "scope": "inventory:read",
  "act": {
    "sub": "https://agents.example.com/order-processor-7f3a",
    "act": {
      "sub": "https://agents.example.com/customer-support-a1b2"
    }
  }
}

Per the RFC, sub identifies the original human on whose behalf the token acts. The outermost act identifies the current actor, the order-processor. The nested act records the prior actor, the customer-support agent that delegated. The scope attenuated at each token exchange, from customer:read to orders:read to inventory:read. The token answers who delegated what to whom. Cedar answers whether that delegation chain is allowed to perform this specific action.

Cedar organizes resources into a hierarchy. A Resource belongs to a ResourceGroup the way a file belongs to a directory. The policy resource in ResourceGroup::"orders" matches any resource in that group. The authorization server maps the token’s claims to Cedar entities at evaluation time: the act.sub becomes the Cedar principal, and the delegation chain populates the request context. The user’s base authorization:

permit(
  principal == User::"jchen",
  action == Action::"read",
  resource
)
when {
  resource in ResourceGroup::"customer-data"
};

This policy grants jchen read access to any resource in the customer-data group, a container that includes orders, returns, profiles, and inventory records.

The customer-support agent receives a narrower capability. It can read orders and returns, not all customer data:

permit(
  principal == Agent::"customer-support-a1b2",
  action == Action::"read",
  resource
)
when {
  context.delegatedBy == User::"jchen" &&
  (resource in ResourceGroup::"orders" ||
   resource in ResourceGroup::"returns")
};

The agent can read resources in orders and returns, two subgroups of customer-data, but not profiles, credentials, or anything else in the parent group. The context.delegatedBy condition ensures this policy applies only when jchen initiated the delegation.

The order-processor receives a narrower capability still. It can read a single inventory record:

permit(
  principal == Agent::"order-processor-7f3a",
  action == Action::"read",
  resource == Resource::"sku-8842"
)
when {
  context.delegatedBy == Agent::"customer-support-a1b2"
};

The scope collapses from an entire resource group to a single resource. The order-processor can read one SKU and nothing else, and only when delegated by the customer-support agent.

The hard boundary that no delegation chain can override:

forbid(
  principal is Agent,
  action,
  resource
)
when {
  resource in ResourceGroup::"credentials"
};

Any request by any agent for any action on any resource in the credentials group, which contains API keys, database passwords, and access tokens, is denied. The forbid overrides every permit in the policy set. No delegation chain, however legitimate, can reach credentials.

At runtime, the authorization server maps the token’s claims into a Cedar authorization request:

{
  "principal": "Agent::order-processor-7f3a",
  "action": "Action::read",
  "resource": "Resource::sku-8842",
  "context": {
    "delegatedBy": "Agent::customer-support-a1b2",
    "originatingUser": "User::jchen"
  }
}

The act.sub from the JWT becomes the Cedar principal. The nested act chain and the sub claim populate the context. Cedar evaluates this request against every policy in the set. The third permit matches: the principal, action, resource, and delegation chain all satisfy the conditions. No forbid fires. The decision is allow. If the same agent requests Resource::aws-credentials, the fourth policy’s forbid fires. The decision is deny. The agent’s reasoning played no role in either decision.

Notice that the policies do not check whether the agent holds a role or group membership. They check whether the delegation chain that produced the request is valid. The authorization question inverts: not “who are you?” but “how did you get here?”

The composition property is what separates this from a tutorial. The forbid policy in the fourth block overrides every permit in the set. This is not a convention that developers must remember to follow. It is a proven invariant of the policy engine. Cedar’s analysis tools can verify that the order-processor’s effective permissions are a strict subset of the customer-support agent’s, which are a strict subset of the user’s. The scope attenuation property holds across the entire policy set, not because someone tested the combinations, but because the engine’s behavior is formally specified.

Four policies are easy to reason about. An enterprise deployment with forty agent types and two hundred policies is not. Forty types against two hundred policies produce eight thousand agent-policy combinations before delegation patterns multiply the space. A new permit policy for a new agent type might interact with an existing forbid in a way no one anticipated. Formal verification guarantees that forbid-trumps-permit holds across all eight thousand combinations, including the ones no one tested because no one imagined them.

Windley’s denial-as-feedback pattern integrates naturally. When the order-processor requests access to a resource outside its scope, Cedar denies the request. In a policy-aware agent loop, the denial becomes structured feedback. The agent replans within the permitted scope rather than failing. For Tier 2 operations in the risk framework from Weighting the Switch, this guided reformulation is the correct behavior. For Tier 3 operations, denial is a wall, not feedback. The tier determines whether the agent gets a second chance.

The tradeoff #

These controls are not free. Someone must author the policies before the first agent runs. The cold start problem is real: you need authorization infrastructure before you deploy agents, and the return is not visible until you operate many agents across trust boundaries. Over-scoping permissions degrades the agent’s usefulness. Under-scoping reintroduces risk. The calibration challenge is the same one I described in Weighting the Switch: start tight and loosen based on evidence.

The strongest objection is ecosystem, not architecture. OPA is a Cloud Native Computing Foundation (CNCF) project with broad adoption across Kubernetes, infrastructure, and application authorization. Rego is Turing-complete and can express arbitrary logic. Cedar trades that expressiveness for the formal guarantees described above. Rego is, as Natoma’s research found, “expressive but error-prone, failing several tests due to runtime exceptions, non-determinism, and extensibility risks.” For agent authorization, you do not want your policy engine to be as expressive as the actor it constrains.

A subtler risk: feeding denial reasons back to the agent, Windley’s denial-as-feedback pattern, can leak information about the policy structure. Recent research on denial-feedback leakage demonstrates that an adversary who can observe the agent’s replanning can use denial messages to map the policy space. The mitigation follows the same principle as authentication error handling: return what was denied, not why. Structured denial codes, not natural language explanations.

Cedar is open source under the Apache 2.0 license. The Lean models are on GitHub. The patterns in this post apply to any policy language with formal guarantees. Cedar is the only one that has them today.

The chain and the court #

Identity answers who. Authorization answers what. In Stamps Without Passports, I defined the six requirements for agent identity: cryptographically verifiable, delegation-aware, scope-attenuated, short-lived, task-specific, and attestable. Cedar enforces those properties. The delegation token carries the chain. The Cedar policy constrains what the chain can do. Together, they provide the formally verified, delegation-aware credential that the blog’s framework requires.

In Starving the Fire, I argued that scoped identity starves the fuel leg of the lethal trifecta. Cedar is the mechanism. A policy that restricts an agent to a single inventory record means a successful prompt injection yields one record for fifteen minutes, not the entire database indefinitely. The economics of the attack collapse.

But what happens when the delegation chain itself is the attack vector? When Agent A’s output becomes Agent B’s untrusted input, and the trifecta emerges across agents rather than within one? Research on tag-along attacks shows that agents which resist direct injection execute payloads from peer agents. Lateral movement through delegated authority does not require new network paths or stolen credentials. It requires a delegation hop. The prize court evaluates each action. It does not yet evaluate the chain.

Thanks for reading Probably Secure. Let’s get to work. Always be curious…all opinions are my own.